(set-option :opt.priority lex)
(set-option :opt.optsmt_engine basic)
(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const r12 Real)
(declare-const r13 Real)
(declare-const r14 Real)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const r18 Real)
(declare-const v20 Bool)
(declare-const r19 Real)
(declare-const v21 Bool)
(declare-const r20 Real)
(declare-const r21 Real)
(assert (or v16 v19))
(assert (or (> r12 93.538196 r18 r21)))
(assert (or v3 (= v10 v3) (= v10 v3)))
(assert (or (= v10 v3) v18))
(assert (or v9))
(assert (or v13))
(assert (or v15 v21))
(assert (or v21))
(assert (or (not v2)))
(assert (or v21 (not v2) v3 v3 v21 (> r19 r6) (> r19 r6) v11 v11 v10 v16))
(assert (or (> r19 r6)))
(assert (or v15 v11))
(assert (or v11 v11 (> r12 93.538196 r18 r21) v10))
(assert (or v13 v3))
(assert (or (> r12 93.538196 r18 r21) v19 (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1) v3 v21 v16 v11))
(assert (or v19))
(assert (or v12 v9 v15))
(assert (or (> r12 93.538196 r18 r21)))
(assert (or v19 v18 v11))
(assert (or v13))
(assert (or v16 v21 (not v2) v9))
(assert (or v18 (not v2) v15))
(assert (or v19 v18 v11 (= v10 v3)))
(assert (or (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1)))
(assert (or (> r12 93.538196 r18 r21) (> r12 93.538196 r18 r21) v21 (> r12 93.538196 r18 r21) v16 (> r12 93.538196 r18 r21) v9 (> r19 r6)))
(assert (or v13))
(assert (or v3 v21 v18 (= v10 v3) (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1) (> r19 r6) v3 v3 v9 (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1) (> r19 r6) (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1)))
(assert (or (= v10 v3)))
(assert (or v19 (> r12 93.538196 r18 r21)))
(assert (or v16))
(assert (or v10 v15 v19 (= v10 v3) v3 v15))
(assert (or v15))
(assert (or v18 v18 v16 (> r12 93.538196 r18 r21) (not v2) v16 v3 (= v10 v3) v11))
(assert (or v11))
(assert (or v10 v13 (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1) (= v10 v3) (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1) (> r19 r6) v10))
(assert (or v11))
(assert (or v21 (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1) (> r19 r6) v21 v18 v15 v19))
(assert (or (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1) v13))
(assert (or v18))
(assert (or v9 v16 v11 v16))
(assert (or v11))
(assert (or v12))
(assert (or v12 v13 v11))
(assert (or v18 (= v10 v3) (xor v10 v11 (not v7) v4 (distinct 0.71968 r4 645.540838 814926.0) v9 v1) v9 v19 v19))
(assert (or v19 v19 v21))
(assert (or v11 v13 v9))
(maximize r0)
(minimize r2)
(minimize r4)
(minimize r7)
(maximize r8)
(minimize r13)
(minimize r14)
(minimize r18)
(maximize r19)
(minimize r20)
(minimize r21)
(check-sat)
